(* -*-sml-*- *)
(*****************************************************************************)
(* Example from FoCs Manual                                                  *)
(* Not for compiling.                                                        *)
(*****************************************************************************)

loadPath := "../official-semantics" :: "../regexp" :: !loadPath;
app load ["bossLib","intLib","regexpLib","ExecuteTools"];

quietdec := true;
open bossLib regexpLib;
quietdec := false;

(******************************************************************************
* Set the trace level of the regular expression library:
* 0: silent
* 1: 1 character (either - or +) for each list element processed
* 2: matches as they are discovered
* 3: transitions as they are calculated
* 4: internal state of the automata
******************************************************************************)
set_trace "regexpTools" 1;

(******************************************************************************
* Set default parsing to natural numbers rather than integers
******************************************************************************)
val _ = intLib.deprecate_int();

(******************************************************************************
* Generated this from a Verilog model of the BUF example in
* Chapter 4 of FoCs User's Manual (see test.v)
* (www.haifa.il.ibm.com/projects/verification/focs/)
******************************************************************************)

(******************************************************************************
* String version
* val StoB_REQ = ``"StoB_REQ"``;
* val BtoS_ACK = ``"BtoS_ACK"``;
* val BtoR_REQ = ``"BtoR_REQ"``;
* val RtoB_ACK = ``"RtoB_ACK"``;
******************************************************************************)

(******************************************************************************
* Num version
******************************************************************************)
val StoB_REQ_def = Define `StoB_REQ = 0`;
val BtoS_ACK_def = Define `BtoS_ACK = 1`;
val BtoR_REQ_def = Define `BtoR_REQ = 2`;
val RtoB_ACK_def = Define `RtoB_ACK = 3`;

quietdec := true;
val SimRun_def =
 Define
  `SimRun =
      [{};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {};
       {StoB_REQ};
       {StoB_REQ; BtoS_ACK};
       {BtoS_ACK};
       {BtoS_ACK; BtoR_REQ};
       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
       {BtoS_ACK; RtoB_ACK};
       {}]`;

quietdec := false;

(******************************************************************************
* Make "&" into an infix for F_AND
******************************************************************************)
val _ = set_fixity "&" (Infixl 500);
val F_AND_IX_def = xDefine "F_AND_IX" `$& f1 f2 = F_AND(f1,f2)`;

(******************************************************************************
* Make ";;" into an infix for S_CAT
******************************************************************************)
val _ = set_fixity ";;" (Infixl 500);
val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`;

(******************************************************************************
* A single property characterising a four-phase handshake
******************************************************************************)
val FOUR_PHASE_def =
 Define
  `FOUR_PHASE req ack =
    F_NEVER
     (S_REPEAT S_TRUE ;;
      S_BOOL(B_AND(B_NOT(B_PROP req),B_PROP ack)) ;;
      S_BOOL(B_PROP req))
    &
    F_NEVER
     (S_REPEAT S_TRUE ;;
      S_BOOL(B_AND(B_PROP req,B_NOT(B_PROP ack))) ;;
      S_BOOL(B_NOT(B_PROP req)))
    &
    F_NEVER
     (S_REPEAT S_TRUE ;;
      S_BOOL(B_AND(B_NOT(B_PROP ack),B_NOT(B_PROP req))) ;;
      S_BOOL(B_PROP ack))
    &
    F_NEVER
     (S_REPEAT S_TRUE ;;
      S_BOOL(B_AND(B_PROP ack,B_PROP req)) ;;
      S_BOOL(B_NOT(B_PROP ack)))`;

(* Version without S_REPEAT S_TRUE
val FOUR_PHASE_def =
 Define
  `FOUR_PHASE req ack =
    F_NEVER
     (
      S_BOOL(B_AND(B_NOT(B_PROP req),B_PROP ack)) ;;
      S_BOOL(B_PROP req))
    &
    F_NEVER
     (
      S_BOOL(B_AND(B_PROP req,B_NOT(B_PROP ack))) ;;
      S_BOOL(B_NOT(B_PROP req)))
    &
    F_NEVER
     (
      S_BOOL(B_AND(B_NOT(B_PROP ack),B_NOT(B_PROP req))) ;;
      S_BOOL(B_PROP ack))
    &
    F_NEVER
     (
      S_BOOL(B_AND(B_PROP ack,B_PROP req)) ;;
      S_BOOL(B_NOT(B_PROP ack)))`;
*)

(******************************************************************************
* Making Verilog finite state machines from FOUR_PHASE regular expressions.
******************************************************************************)
val alph = [``StoB_REQ``, ``BtoS_ACK``, ``BtoR_REQ``, ``RtoB_ACK``];

fun regexp_ra req ack =
  ``sere2regexp
    (S_REPEAT S_TRUE ;;
     S_BOOL(B_AND(B_NOT(B_PROP ^req),B_PROP ^ack)) ;;
     S_BOOL(B_PROP ^req)) : (num -> bool) regexp``;

val r1 = regexp_ra ``StoB_REQ`` ``BtoS_ACK``;

val d1 = try (extract_dfa alph) r1;

val inp1 = {name = "Checker1", alphabet = alph, regexp = r1};

val s1 = print ("\n\n" ^ verilog_dfa inp1 ^ "\n");

val r2 =
  ``sere2regexp
    (S_REPEAT(S_BOOL B_TRUE) ;;
     S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
     S_BOOL(B_PROP BtoS_ACK) ;;
     S_REPEAT(S_BOOL(B_AND(B_PROP BtoS_ACK,
                           B_NOT(B_PROP RtoB_ACK)))) ;;
     S_REPEAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK),
                           B_NOT(B_PROP RtoB_ACK)))) ;;
     S_BOOL(B_PROP BtoS_ACK))``;

val d2 = try (extract_dfa alph) r2;

val inp2 = {name = "Checker2", alphabet = alph, regexp = r2};

val s2 = print ("\n\n" ^ verilog_dfa inp2 ^ "\n");

(******************************************************************************
* vunit four_phase_handskake_left (page 23, FoCs User's Manual, Version 1.0)
* FOUR_PHASE StoB_REQ BtoS_ACK
******************************************************************************)

val four_phase_handskake_left =
 time EVAL ``F_SEM (FINITE SimRun) B_TRUE (FOUR_PHASE StoB_REQ BtoS_ACK)``;

(******************************************************************************
* vunit four_phase_handskake_right (page 24, FoCs User's Manual, Version 1.0)
* FOUR_PHASE BtoR_REQ RtoB_ACK
******************************************************************************)

val four_phase_handskake_right =
time EVAL ``F_SEM (FINITE SimRun) B_TRUE (FOUR_PHASE BtoR_REQ RtoB_ACK)``;

(******************************************************************************
* f1 before f2 = [not f2 W (f1 & not f2)]
******************************************************************************)
val F_BEFORE_def =
 Define
  `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`;

(******************************************************************************
* No underflow: ack1 is asserted between any two ack2 assertions
******************************************************************************)

val ACK_INTERLEAVE_def =
 Define
  `ACK_INTERLEAVE ack1 ack2 =
    F_SUFFIX_IMP
     ((S_REPEAT(S_BOOL B_TRUE) ;;
       S_BOOL(B_NOT(B_PROP ack1)) ;;
       S_BOOL(B_PROP ack1)),
      F_BEFORE
       (F_AND(F_NOT(F_BOOL(B_PROP ack2)),
              F_NEXT(F_BOOL(B_PROP ack2))),
        F_AND(F_NOT(F_BOOL(B_PROP ack1)),
              F_NEXT(F_BOOL(B_PROP ack1)))))`;

(******************************************************************************
* vunit ack_interleaving  (page 22, FoCs User's Manual, Version 1.0)
******************************************************************************)

val ack_interleaving =
 time
  EVAL
  ``F_SEM (FINITE SimRun) B_TRUE (ACK_INTERLEAVE BtoS_ACK RtoB_ACK)
    /\
    F_SEM (FINITE SimRun) B_TRUE (ACK_INTERLEAVE RtoB_ACK BtoS_ACK)``;
